package sketch.specs.symbc;

import gov.nasa.jpf.symbc.Debug;

public class MyClassLong {
	public void myMethod(long x, long y) {
		if(x > 4000) {
			if(y < 900) {
				System.out.println("reach here x y is true");
			} else {
				System.out.println("reach here x true y is false");
			}
		} else {
			if(x + y > 80000) {
				System.out.println("reach here x false y is true");
			} else {
				System.out.println("reach here x false y is false");
			}
		}
	}
	
	// The test driver
	public static void main(String[] args) {
		MyClassLong mc = new MyClassLong();
		mc.myMethod(10l, 20l);
		Debug.printPC("\nMyClassLong.myMethod Path Condition: ");
	}
}
